Verification is typically the most time-consuming component in a circuit design process. Failing to detect functional design errors early in the design stages usually leads to expensive re-spin of the designs. This re-spin includes diagnosis and correction of the errors, logic and physical re-synthesis, and even re-manufacturing of the chips that can be very time-consuming, costly and delay the time-to-market of a product. If the chip designs are already used in some released products, this can even lead to product recalls that are very devastating to a company.
Property checking is an approach for verifying the functionality of a circuit design. It involves proving one or more properties specified for a circuit design. A property, which can also be called an assertion, may be logical (e.g., Boolean) and/or temporal, and describes behavior of one or more signals in the circuit design.
Formal verification of a property verifies that the property holds for all combinations of input signals and sequences over time. For example, to verify that a property holds, formal verification tools or methods attempt to check all states possible during operation of the circuit design, where the operation starts from one or more initial states of the circuit design. Successfully checking all the states ensures that the property is not violated. During the state space search, if a contradiction is found, the property is disproved and a counterexample can usually be generated to demonstrate how the violation occurs.
Formal verification is therefore very useful for uncovering corner-case bugs because it determines whether or not a property is true in the circuit design by exercising all possible behavior of the circuit design. However, due to the exceedingly large and complex circuits that are being designed today, formal verification is subject to the classical state explosion problem. For example, a typical circuit design may contain hundreds of thousands of state variables (state-holding elements, i.e. flip flops), where each state variable may have one of two values, either 0 or 1. The number of possible value combinations (or states) checked by formal verification techniques is extremely large, and some states can only be reached after a very large number of transitions. It is therefore very difficult to perform state space search exhaustively for large designs. Such complexity presents memory and time constraints that make formal verification for large, but typical, circuit designs intractable.
Bounded verification, determines whether or not a property is true in the circuit design for a specific number of transitions. In contrast to the exhaustive search associated with unbounded verification, bounded verification checks the behavior exhaustively for a limited number of transitions. Its main benefit is that the limitation on the number of transitions usually greatly reduces the complexity of the verification problem. However, bounded verification fails to check the behavior beyond the limited number of transitions.
It would be desirable to combine the benefits of limiting the number of transitions checked and yet gain some assurance on the thoroughness of property checking beyond just bounded verification.